package tr.edu.ege.kipler.satisfiability.completion.rules.formula;

import tr.edu.ege.kipler.satisfiability.BranchingException;
import tr.edu.ege.kipler.satisfiability.ReasonerException;
import tr.edu.ege.kipler.satisfiability.Reasoner;
import tr.edu.ege.kipler.satisfiability.UnsatisfiableException;
import tr.edu.ege.kipler.satisfiability.completion.rules.CompletionRule;
import tr.edu.ege.kipler.satisfiability.completion.rules.nondeterminism.OrBranchingPoint;
import tr.edu.ege.kipler.syntax.BinaryBooleanExpression;
import tr.edu.ege.kipler.syntax.WorldElement;
import tr.edu.ege.kipler.syntax.BinaryBooleanExpression.Operator;

/**
 * IMPORTANT: This rule does not have a recursive method to handle multiple
 * levels of disjunctive formulae. It is because each application of the rule
 * branches the tableau tree.
 * 
 * @author İnanç Seylan
 * 
 */
public class DisjunctionRule extends CompletionRule {

	private Reasoner prover;

	private boolean applied;

	public DisjunctionRule(Reasoner prover) {
		this.prover = prover;
	}

	public void apply() throws ReasonerException {
		applied = false;
		for (WorldElement f : getWorld().getPBox().getFormulas()) {
			if (f instanceof BinaryBooleanExpression) {
				BinaryBooleanExpression bf = (BinaryBooleanExpression) f;
				if (bf.getOperator().equals(Operator.OR)
						&& !getWorld().contains(bf.getLhs())
						&& !getWorld().contains(bf.getRhs())) {
					branchForFormulas(bf);
					applied = true;
					throw new BranchingException();
				}
			}
		}
	}

	private void branchForFormulas(BinaryBooleanExpression bf)
			throws UnsatisfiableException {
		OrBranchingPoint bp = new OrBranchingPoint();
		bp.setWcs(getWcs());
		bp.setWorld(getWorld());
		bp.addFormula(bf.getLhs());
		bp.addFormula(bf.getRhs());
		bp.setBranchCause(bf);
		prover.addBranch(bp);
		getWcs().getData().getLogger().info(
				"WCS " + getWcs().getId() + " Disjunction rule: Branching for "
						+ bf.getLhs() + " and " + bf.getRhs());

	}

	/**
	 * @return Returns the applied.
	 */
	public boolean isApplied() {
		return applied;
	}

}
